Exhaustively checking one or more properties in each and every possible state (e.g. of size 1000 bits) and each and every possible input combination to each state by simulation of a digital circuit (e.g. using test vectors) is prohibitively expensive. For this reason, digital circuits (portions thereof or in their entirety) are often analyzed by formal verification, to determine the validity of one or more properties (also called “assertions”) that describe correct and incorrect behaviors in the circuit.
Formal verification of properties can use any of a variety of methods to prove that it is impossible to violate a given property, starting from an initial state of the digital circuit. Tools for formal verification of properties that are available in the prior art (either commercially or from public sources such as universities and laboratories) may be based on any of a number of techniques, such as (1) symbolic model checking, (2) symbolic simulation, (3) explicit state enumeration, and (4) satisfiability (SAT). For background on each of the just-described techniques, see, for example, the following references, each of which is incorporated by reference herein in its entirety:
(1) (a) article by J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang, entitled “Symbolic model checking: 1020 states and beyond”, published in Information and Computation, Vol. 98, no. 2, June 1992; (b) another article entitled “Coverage Estimation for Symbolic Model Checking” by Yatin Hoskote, Timothy Kam, Pei-Hsin Ho, and Xudong Zhao, published in Proceedings of DAC 1999 (Best Paper Award), pp. 300-305, and (c) a PhD thesis by K. L. McMillan entitled “Symbolic model checking—an approach to the state explosion problem”, Carnegie Mellon University, 1992;
(2) article entitled “Automatic Verification of Pipelined Microprocessor Control,” by Jerry R. Burch and David L. Dill, published in the proceedings of International Conference on Computer-Aided Verification, LNCS 818, Springer-Verlag, June 1994;
(3) article entitled by E. M. Clarke, E. A. Emerson and A. P. Sistla entitled “Automatic verification of finite-state concurrent systems using temporal logic specifications” published in ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986;
(4) article entitled “Bounded Model Checking Using Satisfiability Solving” by Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu, published in Formal Methods in System Design, volume 19 issue 1, July 2001, by Kluwer Academic Publishers; and
(5) article entitled “Chaff: Engineering an Efficient SAT Solver” by Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik, published in the Proceedings fo the 38th Design Automation Conference, June 2001.
In addition, see U.S. Pat. No. 5,465,216 granted to Rotem, et al. on Nov. 7, 1995, and entitled “Automatic Design Verification” (that is incorporated by reference herein in its entirety) for an additional example of a formal verification tool. See also U.S. Pat. No. 6,192,505 granted to Beer, et al. on Feb. 20, 2001, and entitled “Method and system for reducing state space variables prior to symbolic model checking” that is incorporated by reference herein in its entirety.
Formal verification tools available in the prior art for property checking include, for example, Symbolic Model Verification (SMV) software package available from Carnegie-Mellon University, the coordinated specification analysis (COSPAN) software package available from Bell Laboratories (e.g. at ftp.research.att.com), and the VIS package available from University of California, Berkeley (e.g. at www-cad.eecs.berkeley.edu/Respep/Research/VIS).
For additional information on formal verification tools, see C. Kern and M. R. Greenstreet, “Formal Verification in Hardware Design: A Survey,” in ACM Trans. on Design Automation of Electronic Systems, vol. 4, pp. 123-193, April 1999 that is incorporated by reference herein in its entirety.
Such formal verification tools normally operate on a description of the digital circuit (also called “circuit-under-verification”), which is generated from a hardware description language (HDL) such as Verilog (see “The Verilog Hardware Description Language,” Third Edition, Don E. Thomas and Philip R. Moorby, Kluwer Academic Publishers, 1996) or VHDL (see “A Guide to VHDL”, Stanley Mazor and Patricia Langstraat, Kluwer Academic Publishers, 1992).
Therefore, during prior art testing of a digital circuit, properties or assertions about the correct and incorrect behaviors of the circuit may be checked using a formal verification tool. The properties are normally described using a HDL language such as Verilog or using a property specification language such as Sugar (e.g. available from IBM Research Labs, Haifa, Israel To validate the correctness of a digital circuit, the formal verification tool must check many properties. The properties may be checked individually sequentially or simultaneously. The formal verification tool may start from a single initial state (or from each of several initial states in a set) for each property.
See U.S. Pat. No. 6,102,959 granted to Hardin, et al. on Aug. 15, 2000 and entitled “Verification tool computation reduction” that is incorporated by reference herein in its entirety.
See also U.S. Pat. No. 6,311,293 granted to Kurshan, et al. on Oct. 30, 2001 and entitled “Detecting of model errors through simplification of model via state reachability analysis” that is incorporated by reference herein in its entirety.
Formal analysis of a property of a digital circuit requires an initial state. In certain prior art, the initial state is commonly chosen to be the reset state of the digital circuit. The reset state is determined by asserting the reset signal of the digital circuit during simulation. More complex circuits may require a sequence of vectors, known as the reset sequence, to place the circuit into the reset state during simulation. Due to the size and complexity of today's digital circuits, a complete formal analysis of the circuit from the reset is not possible due to explosion in the number of potential states in which a digital circuit may exist. For a description of state explosion, see for example, the above-referenced PhD thesis by K. L. McMillan.
Due to the problem of explosion in the number of potential states in which a digital circuit may exist, formal verification tools typically take either of the following approaches to attack the problem of proving a property:                1. design abstraction—perform transformations to reduce and abstract the circuit while ensuring that the formal verification results on the transformed circuit are applicable to the original circuit, see for example, the above-referenced U.S. Pat. No. 6,311,293 granted to Kurshan, et al.; and        2. bounded analysis—entitled “Bounded Model Checking Using Satisfiability Solving” by Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu, published in Formal Methods in System Design, volume 19 issue 1, July 2001, by Kluwer Academic Publishers.        
Various methods of bounded analysis are well known in the art although bounded analysis can use SAT solvers of the type described in “Chaff: Engineering an Efficient SAT Solver” by Matthew W. Moskewicz, et. al., and U.S. Pat. No. 6,292,765 granted to Ho, et. al. on Sep. 18, 2001 and entitled “Method for 10 automatically searching for functional defects in a description of a circuit” that is incorporated by reference herein in its entirety.
Such prior art approaches normally use an initial state (e.g. reset) for formal analysis.